; COMMAND-LINE: --finite-model-find
(set-logic ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun tptp.d () $$unsorted)
(declare-fun tptp.p ($$unsorted $$unsorted) Bool)
(declare-fun tptp.cnf () Bool)
(assert (forall ((A $$unsorted)) (or (tptp.p A tptp.d) tptp.cnf)))
(declare-fun tptp.c () Bool)
(assert (or tptp.cnf tptp.c))
(declare-fun tptp.axiom () $$unsorted)
(assert (forall ((A $$unsorted)) (or (not (tptp.p A tptp.axiom)) (not tptp.c))))
(assert (not (= tptp.axiom tptp.d)))
(assert (not tptp.cnf))
(set-info :filename tptp_parser6)
(check-sat)
